Section: Partnerships and Cooperations

International Initiatives

Inria International Labs

The SACCADES LIAMA project came to a conclusion with the ending of the related Associated Team with ECNU Shanghai. We are actively working on a renewal of this colaboration, integrating the new generation of Professors there.

Inria International Partners

Declared Inria International Partners

• Luigi Liquori has a steady collaboration with researchers from University of Udine, and Turin, Italy.

• We collaborate with the University of Verona on topics of CPS co-simulation. This partly funds a support engineer on their side.

• M.A Peraldi-Frati participates in an international cooperation between University Côte d'Azur, University of Danang (Vietnam) and AUF. This collaboration crystallized through the DNIIT excellence initiative between Univ of Danang and UCA. M.A Peraldi-Frati is involved in the SLEGO project (Specific domain Language for Experience Global Orchestration)[22].

TuMuLT

• Title: Trustworthy Modeling using Logical Time

• International Partner (Institution - Laboratory - Researcher):

  • ECNU (China) - Software Engineering Institute - Min Zhang

• Duration: 2018 - 2022

• Start year: 2018

• See also: https://team.inria.fr/tumult/

• We have four main research directions:

  • Modeling the Uncertain Environments of Cyber-Physical Systems (CPS): Logical Time was one of the main scientific foundations of the AOSTE Team. From the background in theory of concurrency, we are used to consider mainly discrete control systems that can guarantee a functional determinism independently of any implementation-specific timing variation. Addressing CPS means widening those assumptions to consider the external environment as part of the design. The environment obeys the law of physics that usually depend on physical time consideration with models that are approximation of the reality and that necessarily introduce a wide uncertainty on the behavior. This task explores the definition of sound extensions to logical time to capture both the physical continuous behavior and make an abstract characterization as a statistical approximation [25].

  • SMT For Logical Time: While synchronous systems usually focus on finite state-based control systems, our abstraction of logical time relies on both Boolean algebra (for synchronous operations) and integer arithmetic, Solving a system of logical-time constraints is NP-complete but we strive to find efficient algorithms to solve sub-classes of well defined systems. In that context, SMT is a promising solution to combine and solve systems that combine several theories. We had first results on this aspect [8] but we still need to increase the subset of constraints that can be addressed efficiently as well as the performances of the solving tools.

  • Spatio-Temporal Specification for Trustworthy Intelligent Transportation Systems: Focusing on Intelligent Transportation Systems as a subset of Cyber-Physical Systems, we encounter specific problems. In addition to the temporal factor omni-present in real-time and embedded systems, a physical location plays also a central role. Functions of the system (like a train) must be done both at the right time AND at the right location. This task focuses on extensions of our framework for a spatio-temporal logics based on logical time. This means a description of the location of infrastructures as well as the ability to build constraints that depend both on time (logic or physical) and locations (logical or physical).

  • Open pNets: Methods for analyzing and guaranteeing the properties of critical and complex systems, including their data and time depend aspects, have strongly evolved with the emergence of efficient satisfiability checking engines (SAT and SMT). We are working on novel methods combining classical verification paradigms (state-space construction and minimization, model-checking) with SMT approaches to create symbolic and compositional verification methods and tool platforms. We have interesting preliminary results [26], and collaborate actively on both fundamental results and prototype development.

Participation in Other International Programs

• PHC Xu Quangqi funded by ANR for International collaborations with China in 2008.

  • PI: Frédéric Mallet (France) and Zhang Min (China)

  • Title: SMT FOR LOGICAL TIME

  • Description: The main goal of the project was to build an efficient encoding of logical time in SMT solvers. This goal has been achieved (see New Result in Section 7.1).